(set-logic QF_ABV)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const bv_13-0 (_ BitVec 13))
(declare-const arr-5450390008240273326_5450390008240273326-0 (Array (_ BitVec 13) (_ BitVec 13)))
(declare-const arr-5450390008240273326_-9001811012337264657-0 (Array (_ BitVec 13) Bool))
(declare-const arr-5450390008240273326_-9001811012337264657-1 (Array (_ BitVec 13) Bool))
(declare-const v15 Bool)
(declare-const arr-5450390008240273326_4275813681205062635-0 (Array (_ BitVec 13) (Array (_ BitVec 13) Bool)))
(declare-const arr-5450390008240273326_8418138489255711908-0 (Array (_ BitVec 13) (Array (_ BitVec 13) (_ BitVec 13))))
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const bv_12-2 (_ BitVec 12))
(declare-const v21 Bool)
(declare-const arr-5450390008240273326_5450390008240273326-1 (Array (_ BitVec 13) (_ BitVec 13)))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8))
(assert (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v7))
(assert (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v7 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))
(assert (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) v17 v8))
(assert (or v12 (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))
(assert (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v8 (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)))
(assert (or v7 v11 (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))))
(assert (or (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11))
(assert (or v19 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) v12))
(assert (or (bvule bv_13-0 bv_13-0) v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v12 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))
(assert (or v8 v11 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v8 v11))
(assert (or v12 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v7 v10 v4))
(assert (or v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (bvule bv_13-0 bv_13-0)))
(assert (or v17 v10 (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))))
(assert (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v10))
(assert (or v17 v12 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))
(assert (or v8 v10 v10))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (bvule bv_13-0 bv_13-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v12 v7 (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))))
(assert (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (bvule bv_13-0 bv_13-0)))
(assert (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)))
(assert (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v10 v11 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v17 (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 v4))
(assert (or v19 v19 (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)))
(assert (or v8 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v10 v10 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v7 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v8))
(assert (or v19 v17 v10))
(assert (or v12 v10 v10))
(assert (or v17 v12 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))))
(assert (or v8 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) v11))
(assert (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)))
(assert (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) v4 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v4 (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)))
(assert (or v7 v4 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))))
(assert (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)))
(assert (or v4 v8 v4))
(assert (or (or (bvule bv_13-0 bv_13-0) v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))) (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (bvule bv_13-0 bv_13-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (bvule bv_13-0 bv_13-0)) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)) (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) v4 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5))))
(assert (or (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (bvule bv_13-0 bv_13-0)) (or v12 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)) (or v7 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v8) (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v10)))
(assert (and (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v8 v11) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or v12 v10 v10) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5))))
(assert (and (or v17 v10 (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (bvule bv_13-0 bv_13-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or v19 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) v12) (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v8 (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (or v4 v8 v4) (or v17 v12 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v17 (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v7) (and (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v8 v11) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or v12 v10 v10) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))))
(assert (and (or (bvule bv_13-0 bv_13-0) v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))) (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v10) (or v19 v17 v10) (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (or (bvule bv_13-0 bv_13-0) v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0))) (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4))) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (bvule bv_13-0 bv_13-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (bvule bv_13-0 bv_13-0)) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)) (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) v4 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5))) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (bvule bv_13-0 bv_13-0)) (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v4 (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)) (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v12 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)) (and (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v8 v11) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or v12 v10 v10) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)))))
(assert (=> (or v11 (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) v12 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5))))
(assert (or (or v10 v11 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5)) (or v10 v10 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0))))
(assert (or (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v8 v11) (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or v12 (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v11 (bvule bv_13-0 bv_13-0)) (or v19 v17 v10) (and (or (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4) v8 v11) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or v12 v10 v10) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (and v19 v4 v9 v12 (bvule bv_13-0 bv_13-0)) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or v10 v10 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5))) (or v8 (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0)) (or (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v8) (or (not (and v2 v4 v4 v13 v4 v10 v13 v0 v9 v3 v4)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0))))
(assert (or (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (distinct (bvule bv_13-0 bv_13-0) v12 v15 (bvule bv_13-0 bv_13-0) v5) (= v12 v12 (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) (distinct (bvlshr bv_13-0 (bvsrem bv_13-0 bv_13-0)) bv_13-0 (bvsrem bv_13-0 bv_13-0)) (= arr-5450390008240273326_5450390008240273326-0 arr-5450390008240273326_5450390008240273326-0) v16)))
(minimize bv_12-2)
(minimize bv_13-0)
(check-sat)
(exit)
